(declare-fun v5 () Bool)
(declare-fun v9 () Bool)
(declare-fun seq8 () (Seq Int))
(declare-fun seq9 () (Seq Int))
(declare-fun str8 () String)
(assert (or v9 (not v5)))
(assert (xor v9 (seq.prefixof (seq.++ seq8 seq9) seq8)))
(declare-fun i11 () Int)
(check-sat)
(assert (= str8 (str.substr str8 (+ 5 (* i11 (seq.len seq9) (+ 1 1) (+ 1 1))) (* i11 (seq.len seq9) (+ 1 1) (+ 1 1)))))
(check-sat)
